function highlight(cmd){
    document.getElementById(cmd).className = "cmdHighlight";
}

function unhighlight(cmd){
    document.getElementById(cmd).className = "cmdDefault";
}